Nuprl Definition : bframe-p 0,22

@i:k sends only on links in L == e@i. kind(e) = k  (l:IdLnk. (l  L sends(l;e) = nil) 
latex



clarification:

bframe-p(es;i;k;L)
== alle-at(es;i;e.es-kind(ese) = k  Knd
== alle-at(es;i;e. (l:IdLnk.
== alle-at(es;i;e. ((l  L  IdLnk)  es-sends(esle) = nil  es-Msg(es) List)) 
latex


Definitionse@iP(e), Knd, kind(e), x:AB(x), P  Q, A, (x  l), IdLnk, s = t, type List, Msg, sends(l;e), nil
FDL editor aliasesbframe-p

origin